1 /-
2 Copyright (c) 2019 Chris Hughes. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Chris Hughes
5
6 ## Lagrange's four square theorem
7
8 The main result in this file is `sum_four_squares`,
9 a proof that every natural number is the sum of four square numbers.
10
11 # Implementation Notes
12
13 The proof used is close to Lagrange's original proof.
14 -/
15 import data.zmod.basic field_theory.finite group_theory.perm.sign
src └─────────────┘ └─────────────────┘ └────────────────────┘
16 import data.int.parity
src └─────────────┘
17
18 open finset polynomial finite_field equiv
19
20 namespace int
21
22 lemma sum_two_squares_of_two_mul_sum_two_squares {m x y : ℤ} (h : 2 * m = x^2 + y^2) :
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
23 m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
24 have (x^2 + y^2).even, by simp [h.symm, even_mul],
src └────┘ └┘ ┴
typ └────┘ └┘ ┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
25 have hxaddy : (x + y).even, by simpa [pow_two] with parity_simps,
src └─────┘ └─────────────────┘
typ └─────┘ └─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴┴ ┴└────────────────┘
26 have hxsuby : (x - y).even, by simpa [pow_two] with parity_simps,
id └┘ └─────┘
src └┘ └─────┘└─────┘└─────────────────┘
typ └┘ └─────┘└─────┘└─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴┴ ┴└────────────────┘
st └────────────────────────────────┘
27 have (x^2 + y^2) % 2 = 0, by simp [h.symm],
id ┴┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └────┘ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴ └────┘└────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └────────────┘
28 (domain.mul_left_inj (show (2*2 : ℤ) ≠ 0, from dec_trivial)).1 $
id └─────────────────┘ ┴ ┴ ┴ └─────────┘ ┴
src └─────────────────┘ ┴ ┴ ┴ └─────────┘ ┴
typ └─────────────────┘ ┴ ┴ ┴ └─────────┘ ┴
doc └─────────────────┘ └─────────┘
29 calc 2 * 2 * m = (x - y)^2 + (x + y)^2 : by rw [mul_assoc, h]; ring
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└───────┘└┘ ┴ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└───────┘└┘┴┴ └───┘
doc └──┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ ┴
st └────────────┘└─┘┴└─────┘
30 ... = (2 * ((x - y) / 2))^2 + (2 * ((x + y) / 2))^2 :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
31 by rw [int.mul_div_cancel' hxsuby, int.mul_div_cancel' hxaddy]
id └─────────────────┘ └────┘ └─────────────────┘ └────┘
src └──┘└─────────────────┘┴ └┘└─────────────────┘┴ └┘
typ └──┘└─────────────────┘┴└────┘└┘└─────────────────┘┴└────┘└┘
doc └──┘ ┴ └┘ ┴ └┘
txt └──┘ ┴ └┘ ┴ └┘
par └──┘ ┴ └┘ ┴ └┘
pid └┘ ┴ └┘ ┴ ┴┴
st └─────────────────────────────┘└──────────────────────────┘┴┴
32 ... = 2 * 2 * (((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
33 by simp [mul_add, _root_.pow_succ, mul_comm, mul_assoc, mul_left_comm]
id └─────┘ └─────────────┘ └──────┘ └───────┘ └───────────┘
src └────┘└─────┘└┘└─────────────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
typ └────┘└─────┘└┘└─────────────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
doc └────┘ └┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────
34
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
35 lemma exists_sum_two_squares_add_one_eq_k {p : ℕ} (hp : p.prime) :
id ┴ ┴└────┘
src ┴ └────┘
typ ┴ ┴└────┘
doc └────┘
36 ∃ (a b : ℤ) (k : ℕ), a^2 + b^2 + 1 = k * p ∧ k < p :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
37 hp.eq_two_or_odd.elim (λ hp2, hp2.symm ▸ ⟨1, 0, 1, rfl, dec_trivial⟩) $ λ hp1,
id └┘└────────────┘└───┘ └─┘ └─┘└───┘ ┴ └─┘ └─────────┘ └─┘
src └────────────┘└───┘ └───┘ ┴ └─┘ └─────────┘
typ └┘└────────────┘└───┘ └─┘ └─┘└───┘ ┴ └─┘ └─────────┘ └─┘
doc └─────────┘
38 let ⟨a, b, hab⟩ := zmodp.sum_two_squares hp (-1) in
id └─┘ ┴ ┴ └───────────────────┘ └┘ ┴
src └───────────────────┘ ┴
typ └─┘ ┴ ┴ └───────────────────┘ └┘ ┴
39 have hab' : (p : ℤ) ∣ a.val_min_abs ^ 2 + b.val_min_abs ^ 2 + 1,
id ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
src ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
typ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
40 from (zmodp.eq_zero_iff_dvd_int hp _).1 $ by simpa [eq_neg_iff_add_eq_zero] using hab,
id └───────────────────────┘ └┘ ┴ └────────────────────┘ └─┘
src └───────────────────────┘ ┴ └─────┘└────────────────────┘└──────┘
typ └───────────────────────┘ └┘ ┴ └─────┘└────────────────────┘└──────┘└─┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └───────────────────────────────────────┘
41 let ⟨k, hk⟩ := hab' in
id └─┘ ┴ └──┘
typ └─┘ ┴ └──┘
42 have hk0 : 0 ≤ k, from nonneg_of_mul_nonneg_left
id ┴ └───────────────────────┘
src ┴ └───────────────────────┘
typ ┴ └───────────────────────┘
43 (by rw ← hk; exact (add_nonneg (add_nonneg (pow_two_nonneg _) (pow_two_nonneg _)) zero_le_one))
id └┘ └────────┘ └────────────┘ └─────────┘
src └───┘ └────┘ ┴ └────────┘┴ └──┘ └────────────┘└───┘└─────────┘┴
typ └───┘└┘ └────┘ ┴ └────────┘┴ └──┘ └────────────┘└───┘└─────────┘┴
doc └───┘ └────┘ ┴ ┴ └──┘ └───┘ ┴
txt └───┘ └────┘ ┴ ┴ └──┘ └───┘ ┴
par └───┘ └────┘ ┴ ┴ └──┘ └───┘ ┴
pid └─┘ ┴ ┴ ┴ └──┘ └───┘ ┴
st └─────────────────────────────────────────────────────────────────────────────────────────┘
44 (int.coe_nat_pos.2 hp.pos),
id └─────────────┘┴ └┘└──┘
src └─────────────┘┴ └──┘
typ └─────────────┘┴ └┘└──┘
45 ⟨a.val_min_abs, b.val_min_abs, k.nat_abs,
id └──────────┘ └──────────┘ └──────┘
src └──────────┘ └──────────┘ └──────┘
typ └──────────┘ └──────────┘ └──────┘
doc └──────────┘ └──────────┘
46 by rw [hk, int.nat_abs_of_nonneg hk0, mul_comm],
id └┘ └───────────────────┘ └─┘ └──────┘
src └──┘ └┘└───────────────────┘┴ └┘└──────┘┴
typ └──┘└┘└┘└───────────────────┘┴└─┘└┘└──────┘┴
doc └──┘ └┘ ┴ └┘ ┴
txt └──┘ └┘ ┴ └┘ ┴
par └──┘ └┘ ┴ └┘ ┴
pid └┘ └┘ ┴ └┘ ┴
st └─────┘└─────────────────────────┘└────────┘┴
47 lt_of_mul_lt_mul_left
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
48 (calc p * k.nat_abs = a.val_min_abs.nat_abs ^ 2 + b.val_min_abs.nat_abs ^ 2 + 1 :
id ┴ ┴ └──────┘ └──────────┘└──────┘ ┴ ┴ └──────────┘└──────┘ ┴ ┴
src ┴ └──────┘ └──────────┘└──────┘ ┴ ┴ └──────────┘└──────┘ ┴ ┴
typ ┴ ┴ └──────┘ └──────────┘└──────┘ ┴ ┴ └──────────┘└──────┘ ┴ ┴
doc └──────────┘ └──────────┘
49 by rw [← int.coe_nat_inj', int.coe_nat_add, int.coe_nat_add, nat.pow_two, nat.pow_two,
id └──────────────┘ └─────────────┘ └─────────────┘ └─────────┘ └─────────┘
src └────┘└──────────────┘└┘└─────────────┘└┘└─────────────┘└┘└─────────┘└┘└─────────┘└─
typ └────┘└──────────────┘└┘└─────────────┘└┘└─────────────┘└┘└─────────┘└┘└─────────┘└─
doc └────┘ └┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └─
pid └──┘ └┘ └┘ └┘ └┘ └─
st └─────────────────────┘└───────────────┘└───────────────┘└───────────┘└───────────┘└─
50 int.nat_abs_mul_self, int.nat_abs_mul_self, ← _root_.pow_two, ← _root_.pow_two,
id └──────────────────┘ └──────────────────┘ └────────────┘ └────────────┘
src ─────────┘└──────────────────┘└┘└──────────────────┘└──┘└────────────┘└──┘└────────────┘└─
typ ─────────┘└──────────────────┘└┘└──────────────────┘└──┘└────────────┘└──┘└────────────┘└─
doc ─────────┘ └┘ └──┘ └──┘ └─
txt ─────────┘ └┘ └──┘ └──┘ └─
par ─────────┘ └┘ └──┘ └──┘ └─
pid ─────────┘ └┘ └──┘ └──┘ └─
st ─────────────────────────────┘└────────────────────┘└────────────────┘└────────────────┘└─
51 int.coe_nat_one, hk, int.coe_nat_mul, int.nat_abs_of_nonneg hk0]
id └─────────────┘ └┘ └─────────────┘ └───────────────────┘ └─┘
src ─────────┘└─────────────┘└┘ └┘└─────────────┘└┘└───────────────────┘┴ └─
typ ─────────┘└─────────────┘└┘└┘└┘└─────────────┘└┘└───────────────────┘┴└─┘└─
doc ─────────┘ └┘ └┘ └┘ ┴ └─
txt ─────────┘ └┘ └┘ └┘ ┴ └─
par ─────────┘ └┘ └┘ └┘ ┴ └─
pid ─────────┘ └┘ └┘ └┘ ┴ ┴└
st ────────────────────────┘└──┘└───────────────┘└─────────────────────────┘┴└
52 ... ≤ (p / 2) ^ 2 + (p / 2)^2 + 1 :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ─────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘
53 add_le_add
id └────────┘
src └────────┘
typ └────────┘
54 (add_le_add
id └────────┘
src └────────┘
typ └────────┘
55 (nat.pow_le_pow_of_le_left (zmodp.nat_abs_val_min_abs_le _) _)
id └───────────────────────┘ └──────────────────────────┘
src └───────────────────────┘ └──────────────────────────┘
typ └───────────────────────┘ └──────────────────────────┘
56 (nat.pow_le_pow_of_le_left (zmodp.nat_abs_val_min_abs_le _) _))
id └───────────────────────┘ └──────────────────────────┘
src └───────────────────────┘ └──────────────────────────┘
typ └───────────────────────┘ └──────────────────────────┘
57 (le_refl _)
id └─────┘
src └─────┘
typ └─────┘
58 ... < (p / 2) ^ 2 + (p / 2)^ 2 + (p % 2)^2 + ((2 * (p / 2)^2 + (4 * (p / 2) * (p % 2)))) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
59 by rw [hp1, nat.one_pow, mul_one];
id └─┘ └─────────┘ └─────┘
src └──┘ └┘└─────────┘└┘└─────┘┴
typ └──┘└─┘└┘└─────────┘└┘└─────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └──────┘└───────────┘└───────┘┴└─
60 exact (lt_add_iff_pos_right _).2
id └──────────────────┘
src └────┘ └──────────────────┘└─────
typ └────┘ └──────────────────┘└─────
doc └────┘ └─────
txt └────┘ └─────
par └────┘ └─────
pid ┴ └─────
st ───────────────────────────────────────────
61 (add_pos_of_nonneg_of_pos (nat.zero_le _) (mul_pos dec_trivial
id └──────────────────────┘ └─────────┘ └─────┘ └─────────┘
src ───────────┘ └──────────────────────┘┴ └─────────┘└──┘ └─────┘┴└─────────┘└
typ ───────────┘ └──────────────────────┘┴ └─────────┘└──┘ └─────┘┴└─────────┘└
doc ───────────┘ ┴ └──┘ ┴└─────────┘└
txt ───────────┘ ┴ └──┘ ┴ └
par ───────────┘ ┴ └──┘ ┴ └
pid ───────────┘ ┴ └──┘ ┴ └
st ───────────────────────────────────────────────────────────────────────────
62 (nat.div_pos hp.two_le dec_trivial)))
id └─────────┘ └───────┘
src ─────────────┘ └─────────┘┴└───────┘┴ └───
typ ─────────────┘ └─────────┘┴└───────┘┴ └───
doc ─────────────┘ ┴ ┴ └───
txt ─────────────┘ ┴ ┴ └───
par ─────────────┘ ┴ ┴ └───
pid ─────────────┘ ┴ ┴ └─┘└
st ────────────────────────────────────────────────────
63 ... = p * p : begin
id ┴ ┴ ┴
src ─────┘ ┴
typ ─────┘ ┴ ┴ ┴
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘ └─────
64 conv_rhs { rw [← nat.mod_add_div p 2] },
id └─────────────┘ ┴
src └─────────┘└────┘└─────────────┘┴ └──┘┴
typ └─────────┘└────┘└─────────────┘┴┴└──┘┴
txt └─────────┘└────┘ ┴ └──┘┴
par └─────────┘└────┘ ┴ └──┘┴
pid ┴└──────┘ ┴ └───┘
st ─────────────────┘└───────────────────────┘ ┴└┘└
65 simp only [nat.pow_two],
id └─────────┘
src └─────────┘└─────────┘┴
typ └─────────┘└─────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────────┘└─
66 rw [← int.coe_nat_inj'],
id └──────────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └──┘ ┴
st ─────────────────────────────┘└──
67 simp only [nat.pow_two, int.coe_nat_add, int.coe_nat_mul, int.coe_nat_bit0, int.coe_nat_one,
id └─────────┘ └─────────────┘ └─────────────┘ └──────────────┘ └─────────────┘
src └─────────┘└─────────┘└┘└─────────────┘└┘└─────────────┘└┘└──────────────┘└┘└─────────────┘└─
typ └─────────┘└─────────┘└┘└─────────────┘└┘└─────────────┘└┘└──────────────┘└┘└─────────────┘└─
doc └─────────┘ └┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └─
st ─────────────────────────────────────────────────────────────────────────────────────────────────────
68 two_mul, mul_add, add_mul],
id └─────┘ └─────┘ └─────┘
src ─────────┘└─────┘└┘└─────┘└┘└─────┘┴
typ ─────────┘└─────┘└┘└─────┘└┘└─────┘┴
doc ─────────┘ └┘ └┘ ┴
txt ─────────┘ └┘ └┘ ┴
par ─────────┘ └┘ └┘ ┴
pid ─────────┘ └┘ └┘ ┴
st ───────────────────────────────────┘└─
69 ring,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────────┘└─
70 end)
st ────────┘
71 (show 0 ≤ p, from nat.zero_le _)⟩
id ┴ ┴ └─────────┘
src ┴ └─────────┘
typ ┴ ┴ └─────────┘
72
73 end int
74
75 namespace nat
76
77 open int
78
79 open_locale classical
80
81 private lemma sum_four_squares_of_two_mul_sum_four_squares {m a b c d : ℤ}
id ┴
src ┴
typ ┴
82 (h : a^2 + b^2 + c^2 + d^2 = 2 * m) : ∃ w x y z : ℤ, w^2 + x^2 + y^2 + z^2 = m :=
id ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴
83 have ∀ f : fin 4 → zmod 2, (f 0)^2 + (f 1)^2 + (f 2)^2 + (f 3)^2 = 0 →
id └─┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
84 ∃ i : (fin 4), (f i)^2 + f (swap i 0 1)^2 = 0 ∧ f (swap i 0 2)^2 + f (swap i 0 3)^2 = 0,
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
st ┴
85 from dec_trivial,
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
86 let f : fin 4 → ℤ := vector.nth (a::b::c::d::vector.nil) in
id └─┘ ┴ ┴ └────────┘ ┴└┘┴└┘┴└┘┴└┘└────────┘
src └─┘ ┴ └────────┘ └┘ └┘ └┘ └┘└────────┘
typ └─┘ ┴ ┴ └────────┘ ┴└┘┴└┘┴└┘┴└┘└────────┘
87 let ⟨i, hσ⟩ := this (coe ∘ f) (by rw [← @zero_mul (zmod 2) _ m, ← show ((2 : ℤ) : zmod 2) = 0, from rfl,
id └─┘ ┴ └──┘ └─┘ ┴ ┴ └──────┘ └──┘ ┴ └──┘ ┴ └─┘
src └─┘ ┴ └────┘ └──────┘┴ └──┘└────┘ └──┘ ┴ └──┘ └──┘└──┘└──┘┴└───────┘└─┘└─
typ └─┘ ┴ └──┘ └─┘ ┴ ┴ └────┘ └──────┘┴ └──┘└────┘┴└──┘ ┴ └──┘ └──┘└──┘└──┘┴└───────┘└─┘└─
doc └────┘ ┴ └────┘ └──┘ ┴ └──┘ └──┘ └──┘ └───────┘ └─
txt └────┘ ┴ └────┘ └──┘ ┴ └──┘ └──┘ └──┘ └───────┘ └─
par └────┘ ┴ └────┘ └──┘ ┴ └──┘ └──┘ └──┘ └───────┘ └─
pid └──┘ ┴ └────┘ └──┘ ┴ └──┘ └──┘ └──┘ └───────┘ └─
st └───────────────────────────┘└───────────────────────────────────────┘└─
88 ← int.cast_mul, ← h]; simp only [int.cast_add, int.cast_pow]; refl) in
id └──────────┘ ┴ └──────────┘ └──────────┘
src ───┘└──────────┘└──┘ ┴ └─────────┘└──────────┘└┘└──────────┘┴ └──┘
typ ───┘└──────────┘└──┘┴┴ └─────────┘└──────────┘└┘└──────────┘┴ └──┘
doc ───┘ └──┘ ┴ └─────────┘ └┘ ┴ └──┘
txt ───┘ └──┘ ┴ └─────────┘ └┘ ┴ └──┘
par ───┘ └──┘ ┴ └─────────┘ └┘ ┴ └──┘
pid ───┘ └──┘ ┴ ┴└──┘└┘ └┘ ┴
st ───────────────┘└───┘┴└────────────────────────────────────────────┘
89 let σ := swap i 0 in
id ┴ └──┘
src └──┘
typ ┴ └──┘
doc └──┘
90 have h01 : 2 ∣ f (σ 0) ^ 2 + f (σ 1) ^ 2,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
91 from (@zmod.eq_zero_iff_dvd_int 2 _).1 $ by simpa [σ] using hσ.1,
id └──────────────────────┘ ┴ ┴ └┘
src └──────────────────────┘ ┴ └─────┘ └──────┘ └┘
typ └──────────────────────┘ ┴ └─────┘┴└──────┘└┘└┘
doc └─────┘ └──────┘ └┘
txt └─────┘ └──────┘ └┘
par └─────┘ └──────┘ └┘
pid ┴┴ ┴┴└────┘ └┘
st └───────────────────┘
92 have h23 : 2 ∣ f (σ 2) ^ 2 + f (σ 3) ^ 2,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
93 from (@zmod.eq_zero_iff_dvd_int 2 _).1 $ by simpa using hσ.2,
id └──────────────────────┘ ┴ └┘
src └──────────────────────┘ ┴ └──────────┘ └┘
typ └──────────────────────┘ ┴ └──────────┘└┘└┘
doc └──────────┘ └┘
txt └──────────┘ └┘
par └──────────┘ └┘
pid ┴└────┘ └┘
st └───────────────┘
94 let ⟨x, hx⟩ := h01 in let ⟨y, hy⟩ := h23 in
id └─┘ └─┘ └─┘ └─┘
typ └─┘ └─┘ └─┘ └─┘
95 ⟨(f (σ 0) - f (σ 1)) / 2, (f (σ 0) + f (σ 1)) / 2, (f (σ 2) - f (σ 3)) / 2, (f (σ 2) + f (σ 3)) / 2,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
96 begin
st └─────
97 rw [← int.sum_two_squares_of_two_mul_sum_two_squares hx.symm, add_assoc,
id └────────────────────────────────────────────┘ └─────┘ └───────┘
src └────┘└────────────────────────────────────────────┘┴└─────┘└┘└───────┘└─
typ └────┘└────────────────────────────────────────────┘┴└─────┘└┘└───────┘└─
doc └────┘ ┴ └┘ └─
txt └────┘ ┴ └┘ └─
par └────┘ ┴ └┘ └─
pid └──┘ ┴ └┘ └─
st ───────────────────────────────────────────────────────────────┘└─────────┘└─
98 ← int.sum_two_squares_of_two_mul_sum_two_squares hy.symm,
id └────────────────────────────────────────────┘ └─────┘
src ───────┘└────────────────────────────────────────────┘┴└─────┘└─
typ ───────┘└────────────────────────────────────────────┘┴└─────┘└─
doc ───────┘ ┴ └─
txt ───────┘ ┴ └─
par ───────┘ ┴ └─
pid ───────┘ ┴ └─
st ─────────────────────────────────────────────────────────────┘└─
99 ← domain.mul_left_inj (show (2 : ℤ) ≠ 0, from dec_trivial), ← h, mul_add, ← hx, ← hy],
id └─────────────────┘ ┴ └─────────┘ ┴ └─────┘ └┘ └┘
src ───────┘└─────────────────┘┴ ┴ └──┘ └┘┴└───────┘└─────────┘└───┘ └┘└─────┘└──┘ └──┘ ┴
typ ───────┘└─────────────────┘┴ ┴ └──┘ └┘┴└───────┘└─────────┘└───┘┴└┘└─────┘└──┘└┘└──┘└┘┴
doc ───────┘└─────────────────┘┴ ┴ └──┘ └┘ └───────┘└─────────┘└───┘ └┘ └──┘ └──┘ ┴
txt ───────┘ ┴ ┴ └──┘ └┘ └───────┘ └───┘ └┘ └──┘ └──┘ ┴
par ───────┘ ┴ ┴ └──┘ └┘ └───────┘ └───┘ └┘ └──┘ └──┘ ┴
pid ───────┘ ┴ ┴ └──┘ └┘ └───────┘ └───┘ └┘ └──┘ └──┘ ┴
st ───────────────────────────────────────────────────────────────┘└───┘└───────┘└────┘└────┘└──
100 have : univ.sum (λ x, f (σ x)^2) = univ.sum (λ x, f x^2),
id ┴ ┴ └──────┘ ┴
src └─────┘ ┴ └──┘ ┴ ┴ ┴┴└─┘ ┴└──────┘┴ └──┘ ┴ └┘
typ └─────┘ ┴ └──┘ ┴ ┴┴ ┴┴└─┘ ┴└──────┘┴ └──┘┴┴ └┘
doc └─────┘ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴└──────┘┴ └──┘ ┴ └┘
txt └─────┘ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ └┘
par └─────┘ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ └┘
pid └───┘└┘ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ └┘
st ───────────────────────────────────────────────────────────┘└─
101 { conv_rhs { rw finset.sum_univ_perm σ } },
id └──────────────────┘ ┴
src └─────────┘└─┘└──────────────────┘┴ ┴└┘
typ └─────────┘└─┘└──────────────────┘┴┴┴└┘
txt └─────────┘└─┘ ┴ ┴└┘
par └─────────┘└─┘ ┴ ┴└┘
pid ┴└───┘ ┴ └┘┴
st ─────┘└────────┘└─────────────────────────┘┴┴└┘└
102 have fin4univ : (univ : finset (fin 4)).1 = 0::1::2::3::0, from dec_trivial,
id └──┘ └────┘ └─┘ └┘
src └──────────────┘ └──┘└─┘└────┘┴ └─┘└─────┘ └┘└┘┴ ┴ ┴ ┴ └───┘
typ └──────────────┘ └──┘└─┘└────┘┴ └─┘└─────┘ └┘└┘┴ ┴ ┴ ┴ └───┘
doc └──────────────┘ └──┘└─┘└────┘┴ └─────┘ └┘└┘┴ ┴ ┴ ┴ └───┘
txt └──────────────┘ └─┘ ┴ └─────┘ └┘ ┴ ┴ ┴ ┴ └───┘
par └──────────────┘ └─┘ ┴ └─────┘ └┘ ┴ ┴ ┴ ┴ └───┘
pid └───────────┘└─┘ └─┘ ┴ └─────┘ └┘ ┴ ┴ ┴ ┴ └───┘
st ────────────────────────────────────────────────────────────┘└────────────────┘└─
103 simpa [finset.sum_eq_multiset_sum, fin4univ, multiset.sum_cons, f]
id └────────────────────────┘ └──────┘ └───────────────┘ ┴
src └─────┘└────────────────────────┘└┘ └┘└───────────────┘└┘ └─
typ └─────┘└────────────────────────┘└┘└──────┘└┘└───────────────┘└┘┴└─
doc └─────┘ └┘ └┘ └┘ └─
txt └─────┘ └┘ └┘ └┘ └─
par └─────┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ ┴└
st ───────────────────────────────────────────────────────────────────────
104 end⟩
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
105
106 private lemma prime_sum_four_squares {p : ℕ} (hp : p.prime) :
id ┴ ┴└────┘
src ┴ └────┘
typ ┴ ┴└────┘
doc └────┘
107 ∃ a b c d : ℤ, a^2 + b^2 + c^2 + d^2 = p :=
id ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴
src ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴
108 have hm : ∃ m < p, 0 < m ∧ ∃ a b c d : ℤ, a^2 + b^2 + c^2 + d^2 = m * p,
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴
109 from let ⟨a, b, k, hk⟩ := exists_sum_two_squares_add_one_eq_k hp in
id └─┘ ┴ └┘ └─────────────────────────────────┘ └┘
src └─────────────────────────────────┘
typ └─┘ ┴ └┘ └─────────────────────────────────┘ └┘
110 ⟨k, hk.2, nat.pos_of_ne_zero $
id ┴ └────────────────┘
src ┴ └────────────────┘
typ ┴ └────────────────┘
111 (λ hk0, by rw [hk0, int.coe_nat_zero, zero_mul] at hk;
id └─┘ └─┘ └──────────────┘ └──────┘
src └──┘ └┘└──────────────┘└┘└──────┘└─────┘
typ └─┘ └──┘└─┘└┘└──────────────┘└┘└──────┘└─────┘
doc └──┘ └┘ └┘ └─────┘
txt └──┘ └┘ └┘ └─────┘
par └──┘ └┘ └┘ └─────┘
pid └┘ └┘ └┘ ┴└────┘
st └──────┘└────────────────┘└────────┘┴└───────
112 exact ne_of_gt (show a^2 + b^2 + 1 > 0, from add_pos_of_nonneg_of_pos
id └──────┘ ┴┴ ┴ ┴ ┴ └──────────────────────┘
src └────┘└──────┘┴ ┴ ┴└┘ ┴ └┘┴└─┘┴└───────┘└──────────────────────┘└
typ └────┘└──────┘┴ ┴┴┴└┘ ┴┴ └┘┴└─┘┴└───────┘└──────────────────────┘└
doc └────┘ ┴ ┴ └┘ ┴ └┘ └─┘ └───────┘ └
txt └────┘ ┴ ┴ └┘ ┴ └┘ └─┘ └───────┘ └
par └────┘ ┴ ┴ └┘ ┴ └┘ └─┘ └───────┘ └
pid ┴ ┴ ┴ └┘ ┴ └┘ └─┘ └───────┘ └
st ────────────────────────────────────────────────────────────────────────────
113 (add_nonneg (pow_two_nonneg _) (pow_two_nonneg _)) zero_lt_one) hk.1),
id └────────┘ └────────────┘ └─────────┘ └┘
src ───────┘ └────────┘┴ └──┘ └────────────┘└───┘└─────────┘└┘ └┘
typ ───────┘ └────────┘┴ └──┘ └────────────┘└───┘└─────────┘└┘└┘└┘
doc ───────┘ ┴ └──┘ └───┘ └┘ └┘
txt ───────┘ ┴ └──┘ └───┘ └┘ └┘
par ───────┘ ┴ └──┘ └───┘ └┘ └┘
pid ───────┘ ┴ └──┘ └───┘ └┘ └┘
st ───────────────────────────────────────────────────────────────────────────┘
114 a, b, 1, 0, by simpa [_root_.pow_two] using hk.1⟩,
id └────────────┘ └┘
src └─────┘└────────────┘└──────┘ └┘
typ └─────┘└────────────┘└──────┘└┘└┘
doc └─────┘ └──────┘ └┘
txt └─────┘ └──────┘ └┘
par └─────┘ └──────┘ └┘
pid ┴┴ ┴┴└────┘ └┘
st └────────────────────────────────┘
115 let m := nat.find hm in
id ┴ └──────┘ └┘
src └──────┘
typ ┴ └──────┘ └┘
116 let ⟨a, b, c, d, (habcd : a^2 + b^2 + c^2 + d^2 = m * p)⟩ := (nat.find_spec hm).snd.2 in
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ └┘ └─┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ └─┘ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ └┘ └─┘ ┴
117 have hm0 : 0 < m, from (nat.find_spec hm).snd.1,
id ┴ ┴ └───────────┘ └┘ └─┘ ┴
src ┴ └───────────┘ └─┘ ┴
typ ┴ ┴ └───────────┘ └┘ └─┘ ┴
118 have hmp : m < p, from (nat.find_spec hm).fst,
id ┴ ┴ ┴ └───────────┘ └┘ └─┘
src ┴ └───────────┘ └─┘
typ ┴ ┴ ┴ └───────────┘ └┘ └─┘
119 m.mod_two_eq_zero_or_one.elim
id ┴└─────────────────────┘└───┘
src └─────────────────────┘└───┘
typ ┴└─────────────────────┘└───┘
120 (λ hm2 : m % 2 = 0,
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
121 let ⟨k, hk⟩ := (nat.dvd_iff_mod_eq_zero _ _).2 hm2 in
id └─┘ ┴ └─────────────────────┘ ┴ └─┘
src └─────────────────────┘ ┴
typ └─┘ ┴ └─────────────────────┘ ┴ └─┘
122 have hk0 : 0 < k, from nat.pos_of_ne_zero $ λ _, by simp [*, lt_irrefl] at *,
id ┴ └────────────────┘ ┴ └───────┘
src ┴ └────────────────┘ └───────┘└───────┘└────┘
typ ┴ └────────────────┘ ┴ └───────┘└───────┘└────┘
doc └───────┘ └────┘
txt └───────┘ └────┘
par └───────┘ └────┘
pid ┴└──┘ ┴┴└──┘
st └───────────────────────┘
123 have hkm : k < m, by rw [hk, two_mul]; exact (lt_add_iff_pos_left _).2 hk0,
id ┴ ┴ └┘ └─────┘ └─────────────────┘ └─┘
src ┴ └──┘ └┘└─────┘┴ └────┘ └─────────────────┘└────┘
typ ┴ ┴ └──┘└┘└┘└─────┘┴ └────┘ └─────────────────┘└────┘└─┘
doc └──┘ └┘ ┴ └────┘ └────┘
txt └──┘ └┘ ┴ └────┘ └────┘
par └──┘ └┘ ┴ └────┘ └────┘
pid └┘ └┘ ┴ ┴ └────┘
st └─────┘└───────┘┴└───────────────────────────────────┘
124 false.elim $ nat.find_min hm hkm ⟨lt_trans hkm hmp, hk0,
id └────────┘ └──────────┘ └┘ └─┘ └──────┘ └─┘ └─┘ └─┘
src └────────┘ └──────────┘ └──────┘
typ └────────┘ └──────────┘ └┘ └─┘ └──────┘ └─┘ └─┘ └─┘
125 sum_four_squares_of_two_mul_sum_four_squares
id └──────────────────────────────────────────┘
src └──────────────────────────────────────────┘
typ └──────────────────────────────────────────┘
126 (show a^2 + b^2 + c^2 + d^2 = 2 * (k * p),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
127 by rw [habcd, hk, int.coe_nat_mul, mul_assoc]; simp)⟩)
id └───┘ └┘ └─────────────┘ └───────┘
src └──┘ └┘ └┘└─────────────┘└┘└───────┘┴ └──┘
typ └──┘└───┘└┘└┘└┘└─────────────┘└┘└───────┘┴ └──┘
doc └──┘ └┘ └┘ └┘ ┴ └──┘
txt └──┘ └┘ └┘ └┘ ┴ └──┘
par └──┘ └┘ └┘ └┘ ┴ └──┘
pid └┘ └┘ └┘ └┘ ┴
st └────────┘└──┘└───────────────┘└─────────┘┴└────┘
128 (λ hm2 : m % 2 = 1,
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
129 if hm1 : m = 1 then ⟨a, b, c, d, by simp only [hm1, habcd, int.coe_nat_one, one_mul]⟩
id └┘ ┴ ┴ └─┘ └───┘ └─────────────┘ └─────┘
src └┘ ┴ └─────────┘ └┘ └┘└─────────────┘└┘└─────┘┴
typ └┘ ┴ ┴ └─────────┘└─┘└┘└───┘└┘└─────────────┘└┘└─────┘┴
doc └─────────┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st └───────────────────────────────────────────────┘
130 else --have hm1 : 1 < m, from lt_of_le_of_ne hm0 (ne.symm hm1),
131 let mp : ℕ+ := ⟨m, hm0⟩ in
id └─┘ └┘ ┴ └─┘
src └─┘ └┘
typ └─┘ └┘ ┴ └─┘
doc └┘
132 let w := (a : zmod mp).val_min_abs, x := (b : zmod mp).val_min_abs,
id ┴ └──┘ └┘ └─────────┘ ┴ └──┘ └┘ └─────────┘
src └──┘ └─────────┘ └──┘ └─────────┘
typ ┴ └──┘ └┘ └─────────┘ ┴ └──┘ └┘ └─────────┘
doc └─────────┘ └─────────┘
133 y := (c : zmod mp).val_min_abs, z := (d : zmod mp).val_min_abs in
id ┴ └──┘ └┘ └─────────┘ ┴ └──┘ └┘ └─────────┘
src └──┘ └─────────┘ └──┘ └─────────┘
typ ┴ └──┘ └┘ └─────────┘ ┴ └──┘ └┘ └─────────┘
doc └─────────┘ └─────────┘
134 have hnat_abs : w^2 + x^2 + y^2 + z^2 =
id ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴
135 (w.nat_abs^2 + x.nat_abs^2 + y.nat_abs ^2 + z.nat_abs ^ 2 : ℕ),
id ┴└──────┘┴ ┴ ┴└──────┘┴ ┴ ┴└──────┘ ┴ ┴ ┴└──────┘ ┴ ┴
src └──────┘┴ ┴ └──────┘┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
typ ┴└──────┘┴ ┴ ┴└──────┘┴ ┴ ┴└──────┘ ┴ ┴ ┴└──────┘ ┴ ┴
136 by simp [_root_.pow_two],
id └────────────┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └────────────────────┘
137 have hwxyzlt : w^2 + x^2 + y^2 + z^2 < m^2,
id ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴
138 from calc w^2 + x^2 + y^2 + z^2
id ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴
139 = (w.nat_abs^2 + x.nat_abs^2 + y.nat_abs ^2 + z.nat_abs ^ 2 : ℕ) : hnat_abs
id ┴└──────┘┴ ┴ ┴└──────┘┴ ┴ ┴└──────┘ ┴ ┴ ┴└──────┘ ┴ ┴ └──────┘
src └──────┘┴ ┴ └──────┘┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
typ ┴└──────┘┴ ┴ ┴└──────┘┴ ┴ ┴└──────┘ ┴ ┴ ┴└──────┘ ┴ ┴ └──────┘
140 ... ≤ ((m / 2) ^ 2 + (m / 2) ^ 2 + (m / 2) ^ 2 + (m / 2) ^ 2 : ℕ) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
141 int.coe_nat_le.2 $ add_le_add (add_le_add (add_le_add
id └────────────┘┴ └────────┘ └────────┘ └────────┘
src └────────────┘┴ └────────┘ └────────┘ └────────┘
typ └────────────┘┴ └────────┘ └────────┘ └────────┘
142 (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _)
id └───────────────────────┘ └─────────────────────────┘
src └───────────────────────┘ └─────────────────────────┘
typ └───────────────────────┘ └─────────────────────────┘
143 (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _))
id └───────────────────────┘ └─────────────────────────┘
src └───────────────────────┘ └─────────────────────────┘
typ └───────────────────────┘ └─────────────────────────┘
144 (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _))
id └───────────────────────┘ └─────────────────────────┘
src └───────────────────────┘ └─────────────────────────┘
typ └───────────────────────┘ └─────────────────────────┘
145 (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _)
id └───────────────────────┘ └─────────────────────────┘
src └───────────────────────┘ └─────────────────────────┘
typ └───────────────────────┘ └─────────────────────────┘
146 ... = 4 * (m / 2 : ℕ) ^ 2 : by simp [_root_.pow_two, bit0, bit1, mul_add, add_mul]
id ┴ ┴ ┴ ┴ ┴ └────────────┘ └──┘ └──┘ └─────┘ └─────┘
src ┴ ┴ ┴ ┴ └────┘└────────────┘└┘└──┘└┘└──┘└┘└─────┘└┘└─────┘└─
typ ┴ ┴ ┴ ┴ ┴ └────┘└────────────┘└┘└──┘└┘└──┘└┘└─────┘└┘└─────┘└─
doc └────┘ └┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └┘ ┴└
st └────────────────────────────────────────────────────
147 ... < 4 * (m / 2 : ℕ) ^ 2 + ((4 * (m / 2) : ℕ) * (m % 2 : ℕ) + (m % 2 : ℕ)^2) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ───────┘
txt ───────┘
par ───────┘
pid ───────┘
st ───────┘
148 (lt_add_iff_pos_right _).2 (by rw [hm2, int.coe_nat_one, _root_.one_pow, mul_one];
id └──────────────────┘ ┴ └─┘ └─────────────┘ └────────────┘ └─────┘
src └──────────────────┘ ┴ └──┘ └┘└─────────────┘└┘└────────────┘└┘└─────┘┴
typ └──────────────────┘ ┴ └──┘└─┘└┘└─────────────┘└┘└────────────┘└┘└─────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st └──────┘└───────────────┘└──────────────┘└───────┘┴└─
149 exact add_pos_of_nonneg_of_pos (int.coe_nat_nonneg _) zero_lt_one)
id └──────────────────────┘ └────────────────┘ └─────────┘
src └────┘└──────────────────────┘┴ └────────────────┘└──┘└─────────┘
typ └────┘└──────────────────────┘┴ └────────────────┘└──┘└─────────┘
doc └────┘ ┴ └──┘
txt └────┘ ┴ └──┘
par └────┘ ┴ └──┘
pid ┴ ┴ └──┘
st ────────────────────────────────────────────────────────────────────────────┘
150 ... = m ^ 2 : by conv_rhs {rw [← nat.mod_add_div m 2]};
id ┴ ┴ └─────────────┘ ┴
src ┴ └────────┘└────┘└─────────────┘┴ └─┘┴
typ ┴ ┴ └────────┘└────┘└─────────────┘┴┴└─┘┴
txt └────────┘└────┘ ┴ └─┘┴
par └────────┘└────┘ ┴ └─┘┴
pid ┴└─────┘ ┴ └──┘
st └─────────┘└──────────────────────┘ └┘└
151 simp [-nat.mod_add_div, mul_add, add_mul, bit0, bit1, mul_comm, mul_assoc, mul_left_comm,
id └─────┘ └─────┘ └──┘ └──┘ └──────┘ └───────┘ └───────────┘
src └──────────────────────┘└─────┘└┘└─────┘└┘└──┘└┘└──┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
typ └──────────────────────┘└─────┘└┘└─────┘└┘└──┘└┘└──┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
doc └──────────────────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
txt └──────────────────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
par └──────────────────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
pid ┴└─────────────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
st ────────────────────────────────────────────────────────────────────────────────────────────────────
152 _root_.pow_add],
id └────────────┘
src ───────────┘└────────────┘┴
typ ───────────┘└────────────┘┴
doc ───────────┘ ┴
txt ───────────┘ ┴
par ───────────┘ ┴
pid ───────────┘ ┴
st ──────────────────────────┘
153 have hwxyzabcd : ((w^2 + x^2 + y^2 + z^2 : ℤ) : zmod mp) =
id ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ └──┘ └┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ └──┘ └┘ ┴
154 ((a^2 + b^2 + c^2 + d^2 : ℤ) : zmod mp),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘
155 by simp [w, x, y, z, pow_two],
id ┴ ┴ ┴ ┴ └─────┘
src └────┘ └┘ └┘ └┘ └┘└─────┘┴
typ └────┘┴└┘┴└┘┴└┘┴└┘└─────┘┴
doc └────┘ └┘ └┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ └┘ └┘ ┴
par └────┘ └┘ └┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ └┘ └┘ ┴
st └─────────────────────────┘
156 have hwxyz0 : ((w^2 + x^2 + y^2 + z^2 : ℤ) : zmod mp) = 0,
id ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ └──┘ └┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ └──┘ └┘ ┴
157 by rw [hwxyzabcd, habcd, int.cast_mul, show ((m : ℤ) : zmod mp) = (mp : zmod mp), from rfl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
pid └┘
st └───┘
158 int.cast_coe_nat, coe_coe, zmod.cast_self_eq_zero]; simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └────┘
159 let ⟨n, hn⟩ := (zmod.eq_zero_iff_dvd_int.1 hwxyz0) in
id └─┘ ┴ └──────────────────────┘┴ └────┘
src └──────────────────────┘┴
typ └─┘ ┴ └──────────────────────┘┴ └────┘
160 have hn0 : 0 < n.nat_abs, from int.nat_abs_pos_of_ne_zero (λ hn0,
id ┴ └──────┘ └────────────────────────┘ └─┘
src ┴ └──────┘ └────────────────────────┘
typ ┴ └──────┘ └────────────────────────┘ └─┘
161 have hwxyz0 : (w.nat_abs^2 + x.nat_abs^2 + y.nat_abs^2 + z.nat_abs^2 : ℕ) = 0,
id ┴└──────┘┴ ┴ ┴└──────┘┴ ┴ ┴└──────┘┴ ┴ ┴└──────┘┴ ┴ ┴
src └──────┘┴ ┴ └──────┘┴ ┴ └──────┘┴ ┴ └──────┘┴ ┴ ┴
typ ┴└──────┘┴ ┴ ┴└──────┘┴ ┴ ┴└──────┘┴ ┴ ┴└──────┘┴ ┴ ┴
162 by rw [← int.coe_nat_eq_zero, ← hnat_abs]; rwa [hn0, mul_zero] at hn,
163 have habcd0 : (m : ℤ) ∣ a ∧ (m : ℤ) ∣ b ∧ (m : ℤ) ∣ c ∧ (m : ℤ) ∣ d,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
164 by simpa [add_eq_zero_iff_eq_zero_of_nonneg (pow_two_nonneg _) (pow_two_nonneg _),
165 nat.pow_two, w, x, y, z, zmod.eq_zero_iff_dvd_int] using hwxyz0,
166 let ⟨ma, hma⟩ := habcd0.1, ⟨mb, hmb⟩ := habcd0.2.1,
id └─┘ └┘ └────┘┴ └┘ └────┘┴ ┴
src ┴ ┴ ┴
typ └─┘ └┘ └────┘┴ └┘ └────┘┴ ┴
167 ⟨mc, hmc⟩ := habcd0.2.2.1, ⟨md, hmd⟩ := habcd0.2.2.2 in
id └┘ └────┘┴ ┴ ┴ └┘ └────┘┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ └────┘┴ ┴ ┴ └┘ └────┘┴ ┴ ┴
168 have hmdvdp : m ∣ p,
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
169 from int.coe_nat_dvd.1 ⟨ma^2 + mb^2 + mc^2 + md^2,
id └─────────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
170 (domain.mul_left_inj (show (m : ℤ) ≠ 0, from int.coe_nat_ne_zero_iff_pos.2 hm0)).1 $
id └─────────────────┘ ┴ ┴ ┴ └─────────────────────────┘┴ └─┘ ┴
src └─────────────────┘ ┴ ┴ └─────────────────────────┘┴ ┴
typ └─────────────────┘ ┴ ┴ ┴ └─────────────────────────┘┴ └─┘ ┴
doc └─────────────────┘
171 by rw [← habcd, hma, hmb, hmc, hmd]; ring⟩,
172 (hp.2 _ hmdvdp).elim hm1 (λ hmeqp, by simpa [lt_irrefl, hmeqp] using hmp)),
id └┘┴ └────┘ └──┘ └─┘ └───┘
src ┴ └──┘
typ └┘┴ └────┘ └──┘ └─┘ └───┘
173 have hawbxcydz : ((mp : ℕ) : ℤ) ∣ a * w + b * x + c * y + d * z,
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
174 from zmod.eq_zero_iff_dvd_int.1 $ by rw [← hwxyz0]; simp; ring,
id └──────────────────────┘┴
src └──────────────────────┘┴
typ └──────────────────────┘┴
175 have haxbwczdy : ((mp : ℕ) : ℤ) ∣ a * x - b * w - c * z + d * y,
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
176 from zmod.eq_zero_iff_dvd_int.1 $ by simp; ring,
id └──────────────────────┘┴
src └──────────────────────┘┴
typ └──────────────────────┘┴
177 have haybzcwdx : ((mp : ℕ) : ℤ) ∣ a * y + b * z - c * w - d * x,
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
178 from zmod.eq_zero_iff_dvd_int.1 $ by simp; ring,
id └──────────────────────┘┴
src └──────────────────────┘┴
typ └──────────────────────┘┴
179 have hazbycxdw : ((mp : ℕ) : ℤ) ∣ a * z - b * y + c * x - d * w,
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
180 from zmod.eq_zero_iff_dvd_int.1 $ by simp; ring,
id └──────────────────────┘┴
src └──────────────────────┘┴
typ └──────────────────────┘┴
181 let ⟨s, hs⟩ := hawbxcydz, ⟨t, ht⟩ := haxbwczdy, ⟨u, hu⟩ := haybzcwdx, ⟨v, hv⟩ := hazbycxdw in
id └─┘ ┴ └───────┘ ┴ └───────┘ ┴ └───────┘ ┴ └───────┘
typ └─┘ ┴ └───────┘ ┴ └───────┘ ┴ └───────┘ ┴ └───────┘
182 have hn_nonneg : 0 ≤ n,
id ┴
src ┴
typ ┴
183 from nonneg_of_mul_nonneg_left
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
184 (by erw [← hn]; repeat {try {refine add_nonneg _ _}, try {exact pow_two_nonneg _}})
185 (int.coe_nat_pos.2 hm0),
id └─────────────┘┴ └─┘
src └─────────────┘┴
typ └─────────────┘┴ └─┘
186 have hnm : n.nat_abs < mp,
id └──────┘ ┴ └┘
src └──────┘ ┴
typ └──────┘ ┴ └┘
187 from int.coe_nat_lt.1 (lt_of_mul_lt_mul_left
id └────────────┘┴ └───────────────────┘
src └────────────┘┴ └───────────────────┘
typ └────────────┘┴ └───────────────────┘
188 (by rw [int.nat_abs_of_nonneg hn_nonneg, ← hn, ← _root_.pow_two]; exact hwxyzlt)
189 (int.coe_nat_nonneg mp)),
id └────────────────┘ └┘
src └────────────────┘
typ └────────────────┘ └┘
190 have hstuv : s^2 + t^2 + u^2 + v^2 = n.nat_abs * p,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
191 from (domain.mul_left_inj (show (m^2 : ℤ) ≠ 0, from pow_ne_zero 2
id └─────────────────┘ ┴┴ ┴ ┴ └─────────┘
src └─────────────────┘ ┴ ┴ ┴ └─────────┘
typ └─────────────────┘ ┴┴ ┴ ┴ └─────────┘
doc └─────────────────┘
192 (int.coe_nat_ne_zero_iff_pos.2 hm0))).1 $
id └─────────────────────────┘┴ └─┘ ┴
src └─────────────────────────┘┴ ┴
typ └─────────────────────────┘┴ └─┘ ┴
193 calc (m : ℤ)^2 * (s^2 + t^2 + u^2 + v^2) = ((mp : ℕ) * s)^2 + ((mp : ℕ) * t)^2 +
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
194 ((mp : ℕ) * u)^2 + ((mp : ℕ) * v)^2 :
id └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
195 by simp [mp]; ring
196 ... = (w^2 + x^2 + y^2 + z^2) * (a^2 + b^2 + c^2 + d^2) :
id ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
197 by simp only [hs.symm, ht.symm, hu.symm, hv.symm]; ring
198 ... = _ : by rw [hn, habcd, int.nat_abs_of_nonneg hn_nonneg]; dsimp [mp]; ring,
199 false.elim $ nat.find_min hm hnm ⟨lt_trans hnm hmp, hn0, s, t, u, v, hstuv⟩)
id └────────┘ └──────────┘ └┘ └─┘ └──────┘ └─┘ └─┘ └─┘ └───┘
src └────────┘ └──────────┘ └──────┘
typ └────────┘ └──────────┘ └┘ └─┘ └──────┘ └─┘ └─┘ └─┘ └───┘
200
201 lemma sum_four_squares : ∀ n : ℕ, ∃ a b c d : ℕ, a^2 + b^2 + c^2 + d^2 = n
id ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴
202 | 0 := ⟨0, 0, 0, 0, rfl⟩
id └─┘
src └─┘
typ └─┘
203 | 1 := ⟨1, 0, 0, 0, rfl⟩
id └─┘
src └─┘
typ └─┘
204 | n@(k+2) :=
id ┴
src ┴
typ ┴
205 have hm : (min_fac n).prime := min_fac_prime dec_trivial,
id └─────┘ └───┘ └───────────┘ └─────────┘
src └─────┘ └───┘ └───────────┘ └─────────┘
typ └─────┘ └───┘ └───────────┘ └─────────┘
doc └─────┘ └───┘ └─────────┘
206 have n / min_fac n < n := factors_lemma,
id ┴ └─────┘ ┴ └───────────┘
src ┴ └─────┘ ┴ └───────────┘
typ ┴ └─────┘ ┴ └───────────┘
doc └─────┘
207 let ⟨a, b, c, d, h₁⟩ := show ∃ a b c d : ℤ, a^2 + b^2 + c^2 + d^2 = min_fac n,
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ └─────┘
src ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ └─────┘
doc └─────┘
208 from prime_sum_four_squares hm in
id └────────────────────┘ └┘
src └────────────────────┘
typ └────────────────────┘ └┘
209 let ⟨w, x, y, z, h₂⟩ := sum_four_squares (n / min_fac n) in
id └─┘ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └─────┘
src ┴ └─────┘
typ └─┘ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └─────┘
doc └─────┘
210 ⟨(a * x - b * w - c * z + d * y).nat_abs,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
211 (a * y + b * z - c * w - d * x).nat_abs,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
212 (a * z - b * y + c * x - d * w).nat_abs,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
213 (a * w + b * x + c * y + d * z).nat_abs,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
214 begin
215 rw [← int.coe_nat_inj', ← nat.mul_div_cancel' (min_fac_dvd (k+2)), int.coe_nat_mul, ← h₁, ← h₂],
216 simp [nat.pow_two, int.coe_nat_add, int.nat_abs_mul_self'],
217 ring,
st └─
218 end⟩
st ────┘
219
220 end nat